(set-logic QF_BV)
(set-info :source |
This directory contains benchmarks used in the experimental results
reported in the following paper:

Title: Deciding Bit-Vector Arithmetic with Abstraction
Authors: R. E. Bryant, D. Kroening, J. Ouaknine, S. A. Seshia, O. Strichman, B. Brady

If you use these benchmarks, we will appreciate hearing from you by 
e-mail to sseshia@eecs.berkeley.edu. Additionally, the following sources 
must be acknowledged:

1) Y86_std.smt, Y86_btnft.smt: 
   Generated from a UCLID model created by R. E. Bryant, as described
   in the following paper:
    http://www.cs.cmu.edu/~bryant/pubdir/CMU-CS-05-195.pdf

2) s-40-50-bv.smt: 
   Generated by V. Ganapathy for finding format-string exploits in
   the WiSA project (http://www.cs.wisc.edu/wisa)
 
3) BBB-32.smt, rfunit_flat-64.smt:
   Generated from benchmarks generated by Z. Hanna of Intel.

All benchmarks are in the SMT-LIB format, as described at:
http://combination.cs.uiowa.edu/smtlib/

|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status sat)
(declare-fun CVCL_fmt1 () (_ BitVec 32))
(declare-fun CVCL_fmt0 () (_ BitVec 32))
(declare-fun CVCL_ZERO_ () (_ BitVec 32))
(declare-fun CVCL_V_s_count_1 () (_ BitVec 32))
(declare-fun CVCL_V_s_count_2 () (_ BitVec 32))
(declare-fun CVCL_V_s_count_3 () (_ BitVec 32))
(declare-fun CVCL_V_s_count_4 () (_ BitVec 32))
(declare-fun CVCL_V_s_count_5 () (_ BitVec 32))
(declare-fun CVCL_V_s_count_6 () (_ BitVec 32))
(declare-fun CVCL_V_s_count_7 () (_ BitVec 32))
(declare-fun CVCL_V_s_count_8 () (_ BitVec 32))
(declare-fun CVCL_V_s_count_9 () (_ BitVec 32))
(declare-fun CVCL_V_s_count_10 () (_ BitVec 32))
(declare-fun CVCL_V_s_count_11 () (_ BitVec 32))
(declare-fun CVCL_V_s_count_12 () (_ BitVec 32))
(declare-fun CVCL_V_s_count_13 () (_ BitVec 32))
(declare-fun CVCL_V_s_count_14 () (_ BitVec 32))
(declare-fun CVCL_V_s_count_15 () (_ BitVec 32))
(declare-fun CVCL_V_s_count_16 () (_ BitVec 32))
(declare-fun CVCL_V_s_count_17 () (_ BitVec 32))
(declare-fun CVCL_V_s_count_18 () (_ BitVec 32))
(declare-fun CVCL_V_s_count_19 () (_ BitVec 32))
(declare-fun CVCL_V_s_count_20 () (_ BitVec 32))
(declare-fun CVCL_V_s_count_21 () (_ BitVec 32))
(declare-fun CVCL_V_s_count_22 () (_ BitVec 32))
(declare-fun CVCL_V_s_count_23 () (_ BitVec 32))
(declare-fun CVCL_V_s_count_24 () (_ BitVec 32))
(declare-fun CVCL_V_s_count_25 () (_ BitVec 32))
(declare-fun CVCL_V_s_count_26 () (_ BitVec 32))
(declare-fun CVCL_V_s_count_27 () (_ BitVec 32))
(declare-fun CVCL_V_s_count_28 () (_ BitVec 32))
(declare-fun CVCL_V_s_count_29 () (_ BitVec 32))
(declare-fun CVCL_V_s_count_30 () (_ BitVec 32))
(declare-fun CVCL_V_s_count_31 () (_ BitVec 32))
(declare-fun CVCL_V_s_count_32 () (_ BitVec 32))
(declare-fun CVCL_V_s_count_33 () (_ BitVec 32))
(declare-fun CVCL_V_s_count_34 () (_ BitVec 32))
(declare-fun CVCL_V_s_count_35 () (_ BitVec 32))
(declare-fun CVCL_V_s_count_36 () (_ BitVec 32))
(declare-fun CVCL_V_s_count_37 () (_ BitVec 32))
(declare-fun CVCL_V_s_count_38 () (_ BitVec 32))
(declare-fun CVCL_V_s_count_39 () (_ BitVec 32))
(declare-fun CVCL_V_s_count_40 () (_ BitVec 32))
(declare-fun CVCL_V_s_count_41 () (_ BitVec 32))
(declare-fun CVCL_V_format_1 () (_ BitVec 32))
(declare-fun CVCL_V_format_42 () (_ BitVec 32))
(declare-fun CVCL_V_format_2 () (_ BitVec 32))
(declare-fun CVCL_V_format_3 () (_ BitVec 32))
(declare-fun CVCL_V_format_4 () (_ BitVec 32))
(declare-fun CVCL_V_format_5 () (_ BitVec 32))
(declare-fun CVCL_V_format_6 () (_ BitVec 32))
(declare-fun CVCL_V_format_7 () (_ BitVec 32))
(declare-fun CVCL_V_format_8 () (_ BitVec 32))
(declare-fun CVCL_V_format_9 () (_ BitVec 32))
(declare-fun CVCL_V_format_10 () (_ BitVec 32))
(declare-fun CVCL_V_format_11 () (_ BitVec 32))
(declare-fun CVCL_V_format_12 () (_ BitVec 32))
(declare-fun CVCL_V_format_13 () (_ BitVec 32))
(declare-fun CVCL_V_format_14 () (_ BitVec 32))
(declare-fun CVCL_V_format_15 () (_ BitVec 32))
(declare-fun CVCL_V_format_16 () (_ BitVec 32))
(declare-fun CVCL_V_format_17 () (_ BitVec 32))
(declare-fun CVCL_V_format_18 () (_ BitVec 32))
(declare-fun CVCL_V_format_19 () (_ BitVec 32))
(declare-fun CVCL_V_format_20 () (_ BitVec 32))
(declare-fun CVCL_V_format_21 () (_ BitVec 32))
(declare-fun CVCL_V_format_22 () (_ BitVec 32))
(declare-fun CVCL_V_format_23 () (_ BitVec 32))
(declare-fun CVCL_V_format_24 () (_ BitVec 32))
(declare-fun CVCL_V_format_25 () (_ BitVec 32))
(declare-fun CVCL_V_format_26 () (_ BitVec 32))
(declare-fun CVCL_V_format_27 () (_ BitVec 32))
(declare-fun CVCL_V_format_28 () (_ BitVec 32))
(declare-fun CVCL_V_format_29 () (_ BitVec 32))
(declare-fun CVCL_V_format_30 () (_ BitVec 32))
(declare-fun CVCL_V_format_31 () (_ BitVec 32))
(declare-fun CVCL_V_format_32 () (_ BitVec 32))
(declare-fun CVCL_V_format_33 () (_ BitVec 32))
(declare-fun CVCL_V_format_34 () (_ BitVec 32))
(declare-fun CVCL_V_format_35 () (_ BitVec 32))
(declare-fun CVCL_V_format_36 () (_ BitVec 32))
(declare-fun CVCL_V_format_37 () (_ BitVec 32))
(declare-fun CVCL_V_format_38 () (_ BitVec 32))
(declare-fun CVCL_V_format_39 () (_ BitVec 32))
(declare-fun CVCL_V_format_40 () (_ BitVec 32))
(declare-fun CVCL_V_format_41 () (_ BitVec 32))
(declare-fun CVCL_V_format_43 () (_ BitVec 32))
(declare-fun CVCL_arg1 () (_ BitVec 32))
(declare-fun CVCL_V_format_44 () (_ BitVec 32))
(declare-fun CVCL_V_format_45 () (_ BitVec 32))
(declare-fun CVCL_V_format_46 () (_ BitVec 32))
(declare-fun CVCL_V_format_47 () (_ BitVec 32))
(declare-fun CVCL_distance () (_ BitVec 32))
(declare-fun CVCL_fmt_length () (_ BitVec 32))
(declare-fun CVCL_adr_lo () (_ BitVec 32))
(declare-fun CVCL_adr_medlo () (_ BitVec 32))
(declare-fun CVCL_adr_medhi () (_ BitVec 32))
(declare-fun CVCL_adr_hi () (_ BitVec 32))
(declare-fun CVCL_percent () (_ BitVec 32))
(declare-fun CVCL_s () (_ BitVec 32))
(declare-fun CVCL_arg0 () (_ BitVec 32))
(assert (let ((?v_1 ((_ extract 31 0) (_ bv2 32)))) (let ((?v_0 (bvsub (bvadd (bvneg ?v_1) CVCL_fmt1) CVCL_fmt0)) (?v_41 ((_ extract 31 0) (_ bv1 32)))) (let ((?v_2 (bvadd ?v_41 CVCL_ZERO_)) (?v_3 (bvadd ?v_1 CVCL_ZERO_)) (?v_46 ((_ extract 31 0) (_ bv3 32)))) (let ((?v_4 (bvadd ?v_46 CVCL_ZERO_)) (?v_49 ((_ extract 31 0) (_ bv4 32)))) (let ((?v_5 (bvadd ?v_49 CVCL_ZERO_)) (?v_6 (bvadd ((_ extract 31 0) (_ bv5 32)) CVCL_ZERO_)) (?v_7 (bvadd ((_ extract 31 0) (_ bv6 32)) CVCL_ZERO_)) (?v_8 (bvadd ((_ extract 31 0) (_ bv7 32)) CVCL_ZERO_)) (?v_9 (bvadd ((_ extract 31 0) (_ bv8 32)) CVCL_ZERO_)) (?v_10 (bvadd ((_ extract 31 0) (_ bv9 32)) CVCL_ZERO_)) (?v_11 (bvadd ((_ extract 31 0) (_ bv10 32)) CVCL_ZERO_)) (?v_12 (bvadd ((_ extract 31 0) (_ bv11 32)) CVCL_ZERO_)) (?v_13 (bvadd ((_ extract 31 0) (_ bv12 32)) CVCL_ZERO_)) (?v_14 (bvadd ((_ extract 31 0) (_ bv13 32)) CVCL_ZERO_)) (?v_15 (bvadd ((_ extract 31 0) (_ bv14 32)) CVCL_ZERO_)) (?v_16 (bvadd ((_ extract 31 0) (_ bv15 32)) CVCL_ZERO_)) (?v_17 (bvadd ((_ extract 31 0) (_ bv16 32)) CVCL_ZERO_)) (?v_18 (bvadd ((_ extract 31 0) (_ bv17 32)) CVCL_ZERO_)) (?v_19 (bvadd ((_ extract 31 0) (_ bv18 32)) CVCL_ZERO_)) (?v_20 (bvadd ((_ extract 31 0) (_ bv19 32)) CVCL_ZERO_)) (?v_21 (bvadd ((_ extract 31 0) (_ bv20 32)) CVCL_ZERO_)) (?v_22 (bvadd ((_ extract 31 0) (_ bv21 32)) CVCL_ZERO_)) (?v_23 (bvadd ((_ extract 31 0) (_ bv22 32)) CVCL_ZERO_)) (?v_24 (bvadd ((_ extract 31 0) (_ bv23 32)) CVCL_ZERO_)) (?v_25 (bvadd ((_ extract 31 0) (_ bv24 32)) CVCL_ZERO_)) (?v_26 (bvadd ((_ extract 31 0) (_ bv25 32)) CVCL_ZERO_)) (?v_27 (bvadd ((_ extract 31 0) (_ bv26 32)) CVCL_ZERO_)) (?v_28 (bvadd ((_ extract 31 0) (_ bv27 32)) CVCL_ZERO_)) (?v_29 (bvadd ((_ extract 31 0) (_ bv28 32)) CVCL_ZERO_)) (?v_30 (bvadd ((_ extract 31 0) (_ bv29 32)) CVCL_ZERO_)) (?v_31 (bvadd ((_ extract 31 0) (_ bv30 32)) CVCL_ZERO_)) (?v_32 (bvadd ((_ extract 31 0) (_ bv31 32)) CVCL_ZERO_)) (?v_33 (bvadd ((_ extract 31 0) (_ bv32 32)) CVCL_ZERO_)) (?v_34 (bvadd ((_ extract 31 0) (_ bv33 32)) CVCL_ZERO_)) (?v_35 (bvadd ((_ extract 31 0) (_ bv34 32)) CVCL_ZERO_)) (?v_36 (bvadd ((_ extract 31 0) (_ bv35 32)) CVCL_ZERO_)) (?v_37 (bvadd ((_ extract 31 0) (_ bv36 32)) CVCL_ZERO_)) (?v_38 (bvadd ((_ extract 31 0) (_ bv37 32)) CVCL_ZERO_)) (?v_39 (bvadd ((_ extract 31 0) (_ bv38 32)) CVCL_ZERO_)) (?v_40 (bvadd ((_ extract 31 0) (_ bv39 32)) CVCL_ZERO_)) (?v_43 (bvadd ((_ extract 31 0) (_ bv40 32)) CVCL_ZERO_)) (?v_42 (bvadd ?v_41 CVCL_fmt1)) (?v_44 (bvadd ?v_41 CVCL_arg1)) (?v_45 (bvadd ?v_1 CVCL_arg1)) (?v_47 (bvadd ?v_46 CVCL_arg1)) (?v_48 (bvadd CVCL_arg0 CVCL_distance)) (?v_50 (bvadd CVCL_fmt0 CVCL_ZERO_)) (?v_51 (bvadd CVCL_fmt0 ?v_2)) (?v_52 (bvadd CVCL_fmt0 ?v_3)) (?v_53 (bvadd CVCL_fmt0 ?v_4))) (let ((?v_54 (bvadd CVCL_fmt0 ?v_5)) (?v_55 (bvadd CVCL_fmt0 ?v_6)) (?v_56 (bvadd CVCL_fmt0 ?v_7)) (?v_57 (bvadd CVCL_fmt0 ?v_8)) (?v_58 (bvadd CVCL_fmt0 ?v_9)) (?v_59 (bvadd CVCL_fmt0 ?v_10)) (?v_60 (bvadd CVCL_fmt0 ?v_11)) (?v_61 (bvadd CVCL_fmt0 ?v_12)) (?v_62 (bvadd CVCL_fmt0 ?v_13)) (?v_63 (bvadd CVCL_fmt0 ?v_14)) (?v_64 (bvadd CVCL_fmt0 ?v_15)) (?v_65 (bvadd CVCL_fmt0 ?v_16)) (?v_66 (bvadd CVCL_fmt0 ?v_17)) (?v_67 (bvadd CVCL_fmt0 ?v_18)) (?v_68 (bvadd CVCL_fmt0 ?v_19)) (?v_69 (bvadd CVCL_fmt0 ?v_20)) (?v_70 (bvadd CVCL_fmt0 ?v_21)) (?v_71 (bvadd CVCL_fmt0 ?v_22)) (?v_72 (bvadd CVCL_fmt0 ?v_23)) (?v_73 (bvadd CVCL_fmt0 ?v_24)) (?v_74 (bvadd CVCL_fmt0 ?v_25)) (?v_75 (bvadd CVCL_fmt0 ?v_26)) (?v_76 (bvadd CVCL_fmt0 ?v_27)) (?v_77 (bvadd CVCL_fmt0 ?v_28)) (?v_78 (bvadd CVCL_fmt0 ?v_29)) (?v_79 (bvadd CVCL_fmt0 ?v_30)) (?v_80 (bvadd CVCL_fmt0 ?v_31)) (?v_81 (bvadd CVCL_fmt0 ?v_32)) (?v_82 (bvadd CVCL_fmt0 ?v_33)) (?v_83 (bvadd CVCL_fmt0 ?v_34)) (?v_84 (bvadd CVCL_fmt0 ?v_35)) (?v_85 (bvadd CVCL_fmt0 ?v_36)) (?v_86 (bvadd CVCL_fmt0 ?v_37)) (?v_88 (= CVCL_V_format_1 CVCL_percent)) (?v_87 (bvadd ((_ extract 31 0) (_ bv255 32)) CVCL_ZERO_)) (?v_91 (= CVCL_V_format_2 CVCL_percent)) (?v_89 (= CVCL_V_format_2 CVCL_s)) (?v_94 (= CVCL_V_format_3 CVCL_percent)) (?v_92 (= CVCL_V_format_3 CVCL_s)) (?v_97 (= CVCL_V_format_4 CVCL_percent)) (?v_95 (= CVCL_V_format_4 CVCL_s)) (?v_100 (= CVCL_V_format_5 CVCL_percent)) (?v_98 (= CVCL_V_format_5 CVCL_s)) (?v_103 (= CVCL_V_format_6 CVCL_percent)) (?v_101 (= CVCL_V_format_6 CVCL_s)) (?v_106 (= CVCL_V_format_7 CVCL_percent)) (?v_104 (= CVCL_V_format_7 CVCL_s)) (?v_109 (= CVCL_V_format_8 CVCL_percent)) (?v_107 (= CVCL_V_format_8 CVCL_s)) (?v_112 (= CVCL_V_format_9 CVCL_percent)) (?v_110 (= CVCL_V_format_9 CVCL_s)) (?v_115 (= CVCL_V_format_10 CVCL_percent)) (?v_113 (= CVCL_V_format_10 CVCL_s)) (?v_118 (= CVCL_V_format_11 CVCL_percent)) (?v_116 (= CVCL_V_format_11 CVCL_s)) (?v_121 (= CVCL_V_format_12 CVCL_percent)) (?v_119 (= CVCL_V_format_12 CVCL_s)) (?v_124 (= CVCL_V_format_13 CVCL_percent)) (?v_122 (= CVCL_V_format_13 CVCL_s)) (?v_127 (= CVCL_V_format_14 CVCL_percent)) (?v_125 (= CVCL_V_format_14 CVCL_s)) (?v_130 (= CVCL_V_format_15 CVCL_percent)) (?v_128 (= CVCL_V_format_15 CVCL_s)) (?v_133 (= CVCL_V_format_16 CVCL_percent)) (?v_131 (= CVCL_V_format_16 CVCL_s)) (?v_136 (= CVCL_V_format_17 CVCL_percent)) (?v_134 (= CVCL_V_format_17 CVCL_s)) (?v_139 (= CVCL_V_format_18 CVCL_percent)) (?v_137 (= CVCL_V_format_18 CVCL_s)) (?v_142 (= CVCL_V_format_19 CVCL_percent)) (?v_140 (= CVCL_V_format_19 CVCL_s)) (?v_145 (= CVCL_V_format_20 CVCL_percent)) (?v_143 (= CVCL_V_format_20 CVCL_s)) (?v_148 (= CVCL_V_format_21 CVCL_percent)) (?v_146 (= CVCL_V_format_21 CVCL_s)) (?v_151 (= CVCL_V_format_22 CVCL_percent)) (?v_149 (= CVCL_V_format_22 CVCL_s)) (?v_154 (= CVCL_V_format_23 CVCL_percent)) (?v_152 (= CVCL_V_format_23 CVCL_s)) (?v_157 (= CVCL_V_format_24 CVCL_percent)) (?v_155 (= CVCL_V_format_24 CVCL_s)) (?v_160 (= CVCL_V_format_25 CVCL_percent)) (?v_158 (= CVCL_V_format_25 CVCL_s)) (?v_163 (= CVCL_V_format_26 CVCL_percent)) (?v_161 (= CVCL_V_format_26 CVCL_s)) (?v_166 (= CVCL_V_format_27 CVCL_percent)) (?v_164 (= CVCL_V_format_27 CVCL_s)) (?v_169 (= CVCL_V_format_28 CVCL_percent)) (?v_167 (= CVCL_V_format_28 CVCL_s)) (?v_172 (= CVCL_V_format_29 CVCL_percent)) (?v_170 (= CVCL_V_format_29 CVCL_s)) (?v_175 (= CVCL_V_format_30 CVCL_percent)) (?v_173 (= CVCL_V_format_30 CVCL_s)) (?v_178 (= CVCL_V_format_31 CVCL_percent)) (?v_176 (= CVCL_V_format_31 CVCL_s)) (?v_181 (= CVCL_V_format_32 CVCL_percent)) (?v_179 (= CVCL_V_format_32 CVCL_s)) (?v_184 (= CVCL_V_format_33 CVCL_percent)) (?v_182 (= CVCL_V_format_33 CVCL_s)) (?v_187 (= CVCL_V_format_34 CVCL_percent)) (?v_185 (= CVCL_V_format_34 CVCL_s)) (?v_190 (= CVCL_V_format_35 CVCL_percent)) (?v_188 (= CVCL_V_format_35 CVCL_s)) (?v_193 (= CVCL_V_format_36 CVCL_percent)) (?v_191 (= CVCL_V_format_36 CVCL_s)) (?v_196 (= CVCL_V_format_37 CVCL_percent)) (?v_194 (= CVCL_V_format_37 CVCL_s)) (?v_199 (= CVCL_V_format_38 CVCL_percent)) (?v_197 (= CVCL_V_format_38 CVCL_s)) (?v_202 (= CVCL_V_format_39 CVCL_percent)) (?v_200 (= CVCL_V_format_39 CVCL_s)) (?v_205 (= CVCL_V_format_40 CVCL_percent)) (?v_203 (= CVCL_V_format_40 CVCL_s))) (let ((?v_90 (and ?v_88 ?v_89)) (?v_93 (and ?v_91 ?v_92)) (?v_96 (and ?v_94 ?v_95)) (?v_99 (and ?v_97 ?v_98)) (?v_102 (and ?v_100 ?v_101)) (?v_105 (and ?v_103 ?v_104)) (?v_108 (and ?v_106 ?v_107)) (?v_111 (and ?v_109 ?v_110)) (?v_114 (and ?v_112 ?v_113)) (?v_117 (and ?v_115 ?v_116)) (?v_120 (and ?v_118 ?v_119)) (?v_123 (and ?v_121 ?v_122)) (?v_126 (and ?v_124 ?v_125)) (?v_129 (and ?v_127 ?v_128)) (?v_132 (and ?v_130 ?v_131)) (?v_135 (and ?v_133 ?v_134)) (?v_138 (and ?v_136 ?v_137)) (?v_141 (and ?v_139 ?v_140)) (?v_144 (and ?v_142 ?v_143)) (?v_147 (and ?v_145 ?v_146)) (?v_150 (and ?v_148 ?v_149)) (?v_153 (and ?v_151 ?v_152)) (?v_156 (and ?v_154 ?v_155)) (?v_159 (and ?v_157 ?v_158)) (?v_162 (and ?v_160 ?v_161)) (?v_165 (and ?v_163 ?v_164)) (?v_168 (and ?v_166 ?v_167)) (?v_171 (and ?v_169 ?v_170)) (?v_174 (and ?v_172 ?v_173)) (?v_177 (and ?v_175 ?v_176)) (?v_180 (and ?v_178 ?v_179)) (?v_183 (and ?v_181 ?v_182)) (?v_186 (and ?v_184 ?v_185)) (?v_189 (and ?v_187 ?v_188)) (?v_192 (and ?v_190 ?v_191)) (?v_195 (and ?v_193 ?v_194)) (?v_198 (and ?v_196 ?v_197)) (?v_201 (and ?v_199 ?v_200)) (?v_204 (and ?v_202 ?v_203)) (?v_206 (and ?v_205 (= CVCL_V_format_41 CVCL_s)))) (not (or (not (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (or (not (= ?v_0 CVCL_ZERO_)) (= CVCL_V_s_count_1 CVCL_V_s_count_2)) (or (not (= ?v_0 ?v_2)) (= CVCL_V_s_count_1 CVCL_V_s_count_3))) (or (not (= ?v_0 ?v_3)) (= CVCL_V_s_count_1 CVCL_V_s_count_4))) (or (not (= ?v_0 ?v_4)) (= CVCL_V_s_count_1 CVCL_V_s_count_5))) (or (not (= ?v_0 ?v_5)) (= CVCL_V_s_count_1 CVCL_V_s_count_6))) (or (not (= ?v_0 ?v_6)) (= CVCL_V_s_count_1 CVCL_V_s_count_7))) (or (not (= ?v_0 ?v_7)) (= CVCL_V_s_count_1 CVCL_V_s_count_8))) (or (not (= ?v_0 ?v_8)) (= CVCL_V_s_count_1 CVCL_V_s_count_9))) (or (not (= ?v_0 ?v_9)) (= CVCL_V_s_count_1 CVCL_V_s_count_10))) (or (not (= ?v_0 ?v_10)) (= CVCL_V_s_count_1 CVCL_V_s_count_11))) (or (not (= ?v_0 ?v_11)) (= CVCL_V_s_count_1 CVCL_V_s_count_12))) (or (not (= ?v_0 ?v_12)) (= CVCL_V_s_count_1 CVCL_V_s_count_13))) (or (not (= ?v_0 ?v_13)) (= CVCL_V_s_count_1 CVCL_V_s_count_14))) (or (not (= ?v_0 ?v_14)) (= CVCL_V_s_count_1 CVCL_V_s_count_15))) (or (not (= ?v_0 ?v_15)) (= CVCL_V_s_count_1 CVCL_V_s_count_16))) (or (not (= ?v_0 ?v_16)) (= CVCL_V_s_count_1 CVCL_V_s_count_17))) (or (not (= ?v_0 ?v_17)) (= CVCL_V_s_count_1 CVCL_V_s_count_18))) (or (not (= ?v_0 ?v_18)) (= CVCL_V_s_count_1 CVCL_V_s_count_19))) (or (not (= ?v_0 ?v_19)) (= CVCL_V_s_count_1 CVCL_V_s_count_20))) (or (not (= ?v_0 ?v_20)) (= CVCL_V_s_count_1 CVCL_V_s_count_21))) (or (not (= ?v_0 ?v_21)) (= CVCL_V_s_count_1 CVCL_V_s_count_22))) (or (not (= ?v_0 ?v_22)) (= CVCL_V_s_count_1 CVCL_V_s_count_23))) (or (not (= ?v_0 ?v_23)) (= CVCL_V_s_count_1 CVCL_V_s_count_24))) (or (not (= ?v_0 ?v_24)) (= CVCL_V_s_count_1 CVCL_V_s_count_25))) (or (not (= ?v_0 ?v_25)) (= CVCL_V_s_count_1 CVCL_V_s_count_26))) (or (not (= ?v_0 ?v_26)) (= CVCL_V_s_count_1 CVCL_V_s_count_27))) (or (not (= ?v_0 ?v_27)) (= CVCL_V_s_count_1 CVCL_V_s_count_28))) (or (not (= ?v_0 ?v_28)) (= CVCL_V_s_count_1 CVCL_V_s_count_29))) (or (not (= ?v_0 ?v_29)) (= CVCL_V_s_count_1 CVCL_V_s_count_30))) (or (not (= ?v_0 ?v_30)) (= CVCL_V_s_count_1 CVCL_V_s_count_31))) (or (not (= ?v_0 ?v_31)) (= CVCL_V_s_count_1 CVCL_V_s_count_32))) (or (not (= ?v_0 ?v_32)) (= CVCL_V_s_count_1 CVCL_V_s_count_33))) (or (not (= ?v_0 ?v_33)) (= CVCL_V_s_count_1 CVCL_V_s_count_34))) (or (not (= ?v_0 ?v_34)) (= CVCL_V_s_count_1 CVCL_V_s_count_35))) (or (not (= ?v_0 ?v_35)) (= CVCL_V_s_count_1 CVCL_V_s_count_36))) (or (not (= ?v_0 ?v_36)) (= CVCL_V_s_count_1 CVCL_V_s_count_37))) (or (not (= ?v_0 ?v_37)) (= CVCL_V_s_count_1 CVCL_V_s_count_38))) (or (not (= ?v_0 ?v_38)) (= CVCL_V_s_count_1 CVCL_V_s_count_39))) (or (not (= ?v_0 ?v_39)) (= CVCL_V_s_count_1 CVCL_V_s_count_40))) (or (not (= ?v_0 ?v_40)) (= CVCL_V_s_count_1 CVCL_V_s_count_41))) (or (not (= CVCL_ZERO_ CVCL_fmt1)) (= CVCL_V_format_1 CVCL_V_format_42))) (or (not (= ?v_2 CVCL_fmt1)) (= CVCL_V_format_2 CVCL_V_format_42))) (or (not (= ?v_3 CVCL_fmt1)) (= CVCL_V_format_3 CVCL_V_format_42))) (or (not (= ?v_4 CVCL_fmt1)) (= CVCL_V_format_4 CVCL_V_format_42))) (or (not (= ?v_5 CVCL_fmt1)) (= CVCL_V_format_5 CVCL_V_format_42))) (or (not (= ?v_6 CVCL_fmt1)) (= CVCL_V_format_6 CVCL_V_format_42))) (or (not (= ?v_7 CVCL_fmt1)) (= CVCL_V_format_7 CVCL_V_format_42))) (or (not (= ?v_8 CVCL_fmt1)) (= CVCL_V_format_8 CVCL_V_format_42))) (or (not (= ?v_9 CVCL_fmt1)) (= CVCL_V_format_9 CVCL_V_format_42))) (or (not (= ?v_10 CVCL_fmt1)) (= CVCL_V_format_10 CVCL_V_format_42))) (or (not (= ?v_11 CVCL_fmt1)) (= CVCL_V_format_11 CVCL_V_format_42))) (or (not (= ?v_12 CVCL_fmt1)) (= CVCL_V_format_12 CVCL_V_format_42))) (or (not (= ?v_13 CVCL_fmt1)) (= CVCL_V_format_13 CVCL_V_format_42))) (or (not (= ?v_14 CVCL_fmt1)) (= CVCL_V_format_14 CVCL_V_format_42))) (or (not (= ?v_15 CVCL_fmt1)) (= CVCL_V_format_15 CVCL_V_format_42))) (or (not (= ?v_16 CVCL_fmt1)) (= CVCL_V_format_16 CVCL_V_format_42))) (or (not (= ?v_17 CVCL_fmt1)) (= CVCL_V_format_17 CVCL_V_format_42))) (or (not (= ?v_18 CVCL_fmt1)) (= CVCL_V_format_18 CVCL_V_format_42))) (or (not (= ?v_19 CVCL_fmt1)) (= CVCL_V_format_19 CVCL_V_format_42))) (or (not (= ?v_20 CVCL_fmt1)) (= CVCL_V_format_20 CVCL_V_format_42))) (or (not (= ?v_21 CVCL_fmt1)) (= CVCL_V_format_21 CVCL_V_format_42))) (or (not (= ?v_22 CVCL_fmt1)) (= CVCL_V_format_22 CVCL_V_format_42))) (or (not (= ?v_23 CVCL_fmt1)) (= CVCL_V_format_23 CVCL_V_format_42))) (or (not (= ?v_24 CVCL_fmt1)) (= CVCL_V_format_24 CVCL_V_format_42))) (or (not (= ?v_25 CVCL_fmt1)) (= CVCL_V_format_25 CVCL_V_format_42))) (or (not (= ?v_26 CVCL_fmt1)) (= CVCL_V_format_26 CVCL_V_format_42))) (or (not (= ?v_27 CVCL_fmt1)) (= CVCL_V_format_27 CVCL_V_format_42))) (or (not (= ?v_28 CVCL_fmt1)) (= CVCL_V_format_28 CVCL_V_format_42))) (or (not (= ?v_29 CVCL_fmt1)) (= CVCL_V_format_29 CVCL_V_format_42))) (or (not (= ?v_30 CVCL_fmt1)) (= CVCL_V_format_30 CVCL_V_format_42))) (or (not (= ?v_31 CVCL_fmt1)) (= CVCL_V_format_31 CVCL_V_format_42))) (or (not (= ?v_32 CVCL_fmt1)) (= CVCL_V_format_32 CVCL_V_format_42))) (or (not (= ?v_33 CVCL_fmt1)) (= CVCL_V_format_33 CVCL_V_format_42))) (or (not (= ?v_34 CVCL_fmt1)) (= CVCL_V_format_34 CVCL_V_format_42))) (or (not (= ?v_35 CVCL_fmt1)) (= CVCL_V_format_35 CVCL_V_format_42))) (or (not (= ?v_36 CVCL_fmt1)) (= CVCL_V_format_36 CVCL_V_format_42))) (or (not (= ?v_37 CVCL_fmt1)) (= CVCL_V_format_37 CVCL_V_format_42))) (or (not (= ?v_38 CVCL_fmt1)) (= CVCL_V_format_38 CVCL_V_format_42))) (or (not (= ?v_39 CVCL_fmt1)) (= CVCL_V_format_39 CVCL_V_format_42))) (or (not (= ?v_40 CVCL_fmt1)) (= CVCL_V_format_40 CVCL_V_format_42))) (or (not (= ?v_43 CVCL_fmt1)) (= CVCL_V_format_41 CVCL_V_format_42))) (or (not (= CVCL_ZERO_ ?v_42)) (= CVCL_V_format_1 CVCL_V_format_43))) (or (not (= ?v_2 ?v_42)) (= CVCL_V_format_2 CVCL_V_format_43))) (or (not (= ?v_3 ?v_42)) (= CVCL_V_format_3 CVCL_V_format_43))) (or (not (= ?v_4 ?v_42)) (= CVCL_V_format_4 CVCL_V_format_43))) (or (not (= ?v_5 ?v_42)) (= CVCL_V_format_5 CVCL_V_format_43))) (or (not (= ?v_6 ?v_42)) (= CVCL_V_format_6 CVCL_V_format_43))) (or (not (= ?v_7 ?v_42)) (= CVCL_V_format_7 CVCL_V_format_43))) (or (not (= ?v_8 ?v_42)) (= CVCL_V_format_8 CVCL_V_format_43))) (or (not (= ?v_9 ?v_42)) (= CVCL_V_format_9 CVCL_V_format_43))) (or (not (= ?v_10 ?v_42)) (= CVCL_V_format_10 CVCL_V_format_43))) (or (not (= ?v_11 ?v_42)) (= CVCL_V_format_11 CVCL_V_format_43))) (or (not (= ?v_12 ?v_42)) (= CVCL_V_format_12 CVCL_V_format_43))) (or (not (= ?v_13 ?v_42)) (= CVCL_V_format_13 CVCL_V_format_43))) (or (not (= ?v_14 ?v_42)) (= CVCL_V_format_14 CVCL_V_format_43))) (or (not (= ?v_15 ?v_42)) (= CVCL_V_format_15 CVCL_V_format_43))) (or (not (= ?v_16 ?v_42)) (= CVCL_V_format_16 CVCL_V_format_43))) (or (not (= ?v_17 ?v_42)) (= CVCL_V_format_17 CVCL_V_format_43))) (or (not (= ?v_18 ?v_42)) (= CVCL_V_format_18 CVCL_V_format_43))) (or (not (= ?v_19 ?v_42)) (= CVCL_V_format_19 CVCL_V_format_43))) (or (not (= ?v_20 ?v_42)) (= CVCL_V_format_20 CVCL_V_format_43))) (or (not (= ?v_21 ?v_42)) (= CVCL_V_format_21 CVCL_V_format_43))) (or (not (= ?v_22 ?v_42)) (= CVCL_V_format_22 CVCL_V_format_43))) (or (not (= ?v_23 ?v_42)) (= CVCL_V_format_23 CVCL_V_format_43))) (or (not (= ?v_24 ?v_42)) (= CVCL_V_format_24 CVCL_V_format_43))) (or (not (= ?v_25 ?v_42)) (= CVCL_V_format_25 CVCL_V_format_43))) (or (not (= ?v_26 ?v_42)) (= CVCL_V_format_26 CVCL_V_format_43))) (or (not (= ?v_27 ?v_42)) (= CVCL_V_format_27 CVCL_V_format_43))) (or (not (= ?v_28 ?v_42)) (= CVCL_V_format_28 CVCL_V_format_43))) (or (not (= ?v_29 ?v_42)) (= CVCL_V_format_29 CVCL_V_format_43))) (or (not (= ?v_30 ?v_42)) (= CVCL_V_format_30 CVCL_V_format_43))) (or (not (= ?v_31 ?v_42)) (= CVCL_V_format_31 CVCL_V_format_43))) (or (not (= ?v_32 ?v_42)) (= CVCL_V_format_32 CVCL_V_format_43))) (or (not (= ?v_33 ?v_42)) (= CVCL_V_format_33 CVCL_V_format_43))) (or (not (= ?v_34 ?v_42)) (= CVCL_V_format_34 CVCL_V_format_43))) (or (not (= ?v_35 ?v_42)) (= CVCL_V_format_35 CVCL_V_format_43))) (or (not (= ?v_36 ?v_42)) (= CVCL_V_format_36 CVCL_V_format_43))) (or (not (= ?v_37 ?v_42)) (= CVCL_V_format_37 CVCL_V_format_43))) (or (not (= ?v_38 ?v_42)) (= CVCL_V_format_38 CVCL_V_format_43))) (or (not (= ?v_39 ?v_42)) (= CVCL_V_format_39 CVCL_V_format_43))) (or (not (= ?v_40 ?v_42)) (= CVCL_V_format_40 CVCL_V_format_43))) (or (not (= ?v_43 ?v_42)) (= CVCL_V_format_41 CVCL_V_format_43))) (or (not (= CVCL_ZERO_ CVCL_arg1)) (= CVCL_V_format_1 CVCL_V_format_44))) (or (not (= ?v_2 CVCL_arg1)) (= CVCL_V_format_2 CVCL_V_format_44))) (or (not (= ?v_3 CVCL_arg1)) (= CVCL_V_format_3 CVCL_V_format_44))) (or (not (= ?v_4 CVCL_arg1)) (= CVCL_V_format_4 CVCL_V_format_44))) (or (not (= ?v_5 CVCL_arg1)) (= CVCL_V_format_5 CVCL_V_format_44))) (or (not (= ?v_6 CVCL_arg1)) (= CVCL_V_format_6 CVCL_V_format_44))) (or (not (= ?v_7 CVCL_arg1)) (= CVCL_V_format_7 CVCL_V_format_44))) (or (not (= ?v_8 CVCL_arg1)) (= CVCL_V_format_8 CVCL_V_format_44))) (or (not (= ?v_9 CVCL_arg1)) (= CVCL_V_format_9 CVCL_V_format_44))) (or (not (= ?v_10 CVCL_arg1)) (= CVCL_V_format_10 CVCL_V_format_44))) (or (not (= ?v_11 CVCL_arg1)) (= CVCL_V_format_11 CVCL_V_format_44))) (or (not (= ?v_12 CVCL_arg1)) (= CVCL_V_format_12 CVCL_V_format_44))) (or (not (= ?v_13 CVCL_arg1)) (= CVCL_V_format_13 CVCL_V_format_44))) (or (not (= ?v_14 CVCL_arg1)) (= CVCL_V_format_14 CVCL_V_format_44))) (or (not (= ?v_15 CVCL_arg1)) (= CVCL_V_format_15 CVCL_V_format_44))) (or (not (= ?v_16 CVCL_arg1)) (= CVCL_V_format_16 CVCL_V_format_44))) (or (not (= ?v_17 CVCL_arg1)) (= CVCL_V_format_17 CVCL_V_format_44))) (or (not (= ?v_18 CVCL_arg1)) (= CVCL_V_format_18 CVCL_V_format_44))) (or (not (= ?v_19 CVCL_arg1)) (= CVCL_V_format_19 CVCL_V_format_44))) (or (not (= ?v_20 CVCL_arg1)) (= CVCL_V_format_20 CVCL_V_format_44))) (or (not (= ?v_21 CVCL_arg1)) (= CVCL_V_format_21 CVCL_V_format_44))) (or (not (= ?v_22 CVCL_arg1)) (= CVCL_V_format_22 CVCL_V_format_44))) (or (not (= ?v_23 CVCL_arg1)) (= CVCL_V_format_23 CVCL_V_format_44))) (or (not (= ?v_24 CVCL_arg1)) (= CVCL_V_format_24 CVCL_V_format_44))) (or (not (= ?v_25 CVCL_arg1)) (= CVCL_V_format_25 CVCL_V_format_44))) (or (not (= ?v_26 CVCL_arg1)) (= CVCL_V_format_26 CVCL_V_format_44))) (or (not (= ?v_27 CVCL_arg1)) (= CVCL_V_format_27 CVCL_V_format_44))) (or (not (= ?v_28 CVCL_arg1)) (= CVCL_V_format_28 CVCL_V_format_44))) (or (not (= ?v_29 CVCL_arg1)) (= CVCL_V_format_29 CVCL_V_format_44))) (or (not (= ?v_30 CVCL_arg1)) (= CVCL_V_format_30 CVCL_V_format_44))) (or (not (= ?v_31 CVCL_arg1)) (= CVCL_V_format_31 CVCL_V_format_44))) (or (not (= ?v_32 CVCL_arg1)) (= CVCL_V_format_32 CVCL_V_format_44))) (or (not (= ?v_33 CVCL_arg1)) (= CVCL_V_format_33 CVCL_V_format_44))) (or (not (= ?v_34 CVCL_arg1)) (= CVCL_V_format_34 CVCL_V_format_44))) (or (not (= ?v_35 CVCL_arg1)) (= CVCL_V_format_35 CVCL_V_format_44))) (or (not (= ?v_36 CVCL_arg1)) (= CVCL_V_format_36 CVCL_V_format_44))) (or (not (= ?v_37 CVCL_arg1)) (= CVCL_V_format_37 CVCL_V_format_44))) (or (not (= ?v_38 CVCL_arg1)) (= CVCL_V_format_38 CVCL_V_format_44))) (or (not (= ?v_39 CVCL_arg1)) (= CVCL_V_format_39 CVCL_V_format_44))) (or (not (= ?v_40 CVCL_arg1)) (= CVCL_V_format_40 CVCL_V_format_44))) (or (not (= ?v_43 CVCL_arg1)) (= CVCL_V_format_41 CVCL_V_format_44))) (or (not (= CVCL_fmt1 CVCL_arg1)) (= CVCL_V_format_42 CVCL_V_format_44))) (or (not (= ?v_42 CVCL_arg1)) (= CVCL_V_format_43 CVCL_V_format_44))) (or (not (= CVCL_ZERO_ ?v_44)) (= CVCL_V_format_1 CVCL_V_format_45))) (or (not (= ?v_2 ?v_44)) (= CVCL_V_format_2 CVCL_V_format_45))) (or (not (= ?v_3 ?v_44)) (= CVCL_V_format_3 CVCL_V_format_45))) (or (not (= ?v_4 ?v_44)) (= CVCL_V_format_4 CVCL_V_format_45))) (or (not (= ?v_5 ?v_44)) (= CVCL_V_format_5 CVCL_V_format_45))) (or (not (= ?v_6 ?v_44)) (= CVCL_V_format_6 CVCL_V_format_45))) (or (not (= ?v_7 ?v_44)) (= CVCL_V_format_7 CVCL_V_format_45))) (or (not (= ?v_8 ?v_44)) (= CVCL_V_format_8 CVCL_V_format_45))) (or (not (= ?v_9 ?v_44)) (= CVCL_V_format_9 CVCL_V_format_45))) (or (not (= ?v_10 ?v_44)) (= CVCL_V_format_10 CVCL_V_format_45))) (or (not (= ?v_11 ?v_44)) (= CVCL_V_format_11 CVCL_V_format_45))) (or (not (= ?v_12 ?v_44)) (= CVCL_V_format_12 CVCL_V_format_45))) (or (not (= ?v_13 ?v_44)) (= CVCL_V_format_13 CVCL_V_format_45))) (or (not (= ?v_14 ?v_44)) (= CVCL_V_format_14 CVCL_V_format_45))) (or (not (= ?v_15 ?v_44)) (= CVCL_V_format_15 CVCL_V_format_45))) (or (not (= ?v_16 ?v_44)) (= CVCL_V_format_16 CVCL_V_format_45))) (or (not (= ?v_17 ?v_44)) (= CVCL_V_format_17 CVCL_V_format_45))) (or (not (= ?v_18 ?v_44)) (= CVCL_V_format_18 CVCL_V_format_45))) (or (not (= ?v_19 ?v_44)) (= CVCL_V_format_19 CVCL_V_format_45))) (or (not (= ?v_20 ?v_44)) (= CVCL_V_format_20 CVCL_V_format_45))) (or (not (= ?v_21 ?v_44)) (= CVCL_V_format_21 CVCL_V_format_45))) (or (not (= ?v_22 ?v_44)) (= CVCL_V_format_22 CVCL_V_format_45))) (or (not (= ?v_23 ?v_44)) (= CVCL_V_format_23 CVCL_V_format_45))) (or (not (= ?v_24 ?v_44)) (= CVCL_V_format_24 CVCL_V_format_45))) (or (not (= ?v_25 ?v_44)) (= CVCL_V_format_25 CVCL_V_format_45))) (or (not (= ?v_26 ?v_44)) (= CVCL_V_format_26 CVCL_V_format_45))) (or (not (= ?v_27 ?v_44)) (= CVCL_V_format_27 CVCL_V_format_45))) (or (not (= ?v_28 ?v_44)) (= CVCL_V_format_28 CVCL_V_format_45))) (or (not (= ?v_29 ?v_44)) (= CVCL_V_format_29 CVCL_V_format_45))) (or (not (= ?v_30 ?v_44)) (= CVCL_V_format_30 CVCL_V_format_45))) (or (not (= ?v_31 ?v_44)) (= CVCL_V_format_31 CVCL_V_format_45))) (or (not (= ?v_32 ?v_44)) (= CVCL_V_format_32 CVCL_V_format_45))) (or (not (= ?v_33 ?v_44)) (= CVCL_V_format_33 CVCL_V_format_45))) (or (not (= ?v_34 ?v_44)) (= CVCL_V_format_34 CVCL_V_format_45))) (or (not (= ?v_35 ?v_44)) (= CVCL_V_format_35 CVCL_V_format_45))) (or (not (= ?v_36 ?v_44)) (= CVCL_V_format_36 CVCL_V_format_45))) (or (not (= ?v_37 ?v_44)) (= CVCL_V_format_37 CVCL_V_format_45))) (or (not (= ?v_38 ?v_44)) (= CVCL_V_format_38 CVCL_V_format_45))) (or (not (= ?v_39 ?v_44)) (= CVCL_V_format_39 CVCL_V_format_45))) (or (not (= ?v_40 ?v_44)) (= CVCL_V_format_40 CVCL_V_format_45))) (or (not (= ?v_43 ?v_44)) (= CVCL_V_format_41 CVCL_V_format_45))) (or (not (= CVCL_fmt1 ?v_44)) (= CVCL_V_format_42 CVCL_V_format_45))) (or (not (= ?v_42 ?v_44)) (= CVCL_V_format_43 CVCL_V_format_45))) (or (not (= CVCL_ZERO_ ?v_45)) (= CVCL_V_format_1 CVCL_V_format_46))) (or (not (= ?v_2 ?v_45)) (= CVCL_V_format_2 CVCL_V_format_46))) (or (not (= ?v_3 ?v_45)) (= CVCL_V_format_3 CVCL_V_format_46))) (or (not (= ?v_4 ?v_45)) (= CVCL_V_format_4 CVCL_V_format_46))) (or (not (= ?v_5 ?v_45)) (= CVCL_V_format_5 CVCL_V_format_46))) (or (not (= ?v_6 ?v_45)) (= CVCL_V_format_6 CVCL_V_format_46))) (or (not (= ?v_7 ?v_45)) (= CVCL_V_format_7 CVCL_V_format_46))) (or (not (= ?v_8 ?v_45)) (= CVCL_V_format_8 CVCL_V_format_46))) (or (not (= ?v_9 ?v_45)) (= CVCL_V_format_9 CVCL_V_format_46))) (or (not (= ?v_10 ?v_45)) (= CVCL_V_format_10 CVCL_V_format_46))) (or (not (= ?v_11 ?v_45)) (= CVCL_V_format_11 CVCL_V_format_46))) (or (not (= ?v_12 ?v_45)) (= CVCL_V_format_12 CVCL_V_format_46))) (or (not (= ?v_13 ?v_45)) (= CVCL_V_format_13 CVCL_V_format_46))) (or (not (= ?v_14 ?v_45)) (= CVCL_V_format_14 CVCL_V_format_46))) (or (not (= ?v_15 ?v_45)) (= CVCL_V_format_15 CVCL_V_format_46))) (or (not (= ?v_16 ?v_45)) (= CVCL_V_format_16 CVCL_V_format_46))) (or (not (= ?v_17 ?v_45)) (= CVCL_V_format_17 CVCL_V_format_46))) (or (not (= ?v_18 ?v_45)) (= CVCL_V_format_18 CVCL_V_format_46))) (or (not (= ?v_19 ?v_45)) (= CVCL_V_format_19 CVCL_V_format_46))) (or (not (= ?v_20 ?v_45)) (= CVCL_V_format_20 CVCL_V_format_46))) (or (not (= ?v_21 ?v_45)) (= CVCL_V_format_21 CVCL_V_format_46))) (or (not (= ?v_22 ?v_45)) (= CVCL_V_format_22 CVCL_V_format_46))) (or (not (= ?v_23 ?v_45)) (= CVCL_V_format_23 CVCL_V_format_46))) (or (not (= ?v_24 ?v_45)) (= CVCL_V_format_24 CVCL_V_format_46))) (or (not (= ?v_25 ?v_45)) (= CVCL_V_format_25 CVCL_V_format_46))) (or (not (= ?v_26 ?v_45)) (= CVCL_V_format_26 CVCL_V_format_46))) (or (not (= ?v_27 ?v_45)) (= CVCL_V_format_27 CVCL_V_format_46))) (or (not (= ?v_28 ?v_45)) (= CVCL_V_format_28 CVCL_V_format_46))) (or (not (= ?v_29 ?v_45)) (= CVCL_V_format_29 CVCL_V_format_46))) (or (not (= ?v_30 ?v_45)) (= CVCL_V_format_30 CVCL_V_format_46))) (or (not (= ?v_31 ?v_45)) (= CVCL_V_format_31 CVCL_V_format_46))) (or (not (= ?v_32 ?v_45)) (= CVCL_V_format_32 CVCL_V_format_46))) (or (not (= ?v_33 ?v_45)) (= CVCL_V_format_33 CVCL_V_format_46))) (or (not (= ?v_34 ?v_45)) (= CVCL_V_format_34 CVCL_V_format_46))) (or (not (= ?v_35 ?v_45)) (= CVCL_V_format_35 CVCL_V_format_46))) (or (not (= ?v_36 ?v_45)) (= CVCL_V_format_36 CVCL_V_format_46))) (or (not (= ?v_37 ?v_45)) (= CVCL_V_format_37 CVCL_V_format_46))) (or (not (= ?v_38 ?v_45)) (= CVCL_V_format_38 CVCL_V_format_46))) (or (not (= ?v_39 ?v_45)) (= CVCL_V_format_39 CVCL_V_format_46))) (or (not (= ?v_40 ?v_45)) (= CVCL_V_format_40 CVCL_V_format_46))) (or (not (= ?v_43 ?v_45)) (= CVCL_V_format_41 CVCL_V_format_46))) (or (not (= CVCL_fmt1 ?v_45)) (= CVCL_V_format_42 CVCL_V_format_46))) (or (not (= ?v_42 ?v_45)) (= CVCL_V_format_43 CVCL_V_format_46))) (or (not (= CVCL_ZERO_ ?v_47)) (= CVCL_V_format_1 CVCL_V_format_47))) (or (not (= ?v_2 ?v_47)) (= CVCL_V_format_2 CVCL_V_format_47))) (or (not (= ?v_3 ?v_47)) (= CVCL_V_format_3 CVCL_V_format_47))) (or (not (= ?v_4 ?v_47)) (= CVCL_V_format_4 CVCL_V_format_47))) (or (not (= ?v_5 ?v_47)) (= CVCL_V_format_5 CVCL_V_format_47))) (or (not (= ?v_6 ?v_47)) (= CVCL_V_format_6 CVCL_V_format_47))) (or (not (= ?v_7 ?v_47)) (= CVCL_V_format_7 CVCL_V_format_47))) (or (not (= ?v_8 ?v_47)) (= CVCL_V_format_8 CVCL_V_format_47))) (or (not (= ?v_9 ?v_47)) (= CVCL_V_format_9 CVCL_V_format_47))) (or (not (= ?v_10 ?v_47)) (= CVCL_V_format_10 CVCL_V_format_47))) (or (not (= ?v_11 ?v_47)) (= CVCL_V_format_11 CVCL_V_format_47))) (or (not (= ?v_12 ?v_47)) (= CVCL_V_format_12 CVCL_V_format_47))) (or (not (= ?v_13 ?v_47)) (= CVCL_V_format_13 CVCL_V_format_47))) (or (not (= ?v_14 ?v_47)) (= CVCL_V_format_14 CVCL_V_format_47))) (or (not (= ?v_15 ?v_47)) (= CVCL_V_format_15 CVCL_V_format_47))) (or (not (= ?v_16 ?v_47)) (= CVCL_V_format_16 CVCL_V_format_47))) (or (not (= ?v_17 ?v_47)) (= CVCL_V_format_17 CVCL_V_format_47))) (or (not (= ?v_18 ?v_47)) (= CVCL_V_format_18 CVCL_V_format_47))) (or (not (= ?v_19 ?v_47)) (= CVCL_V_format_19 CVCL_V_format_47))) (or (not (= ?v_20 ?v_47)) (= CVCL_V_format_20 CVCL_V_format_47))) (or (not (= ?v_21 ?v_47)) (= CVCL_V_format_21 CVCL_V_format_47))) (or (not (= ?v_22 ?v_47)) (= CVCL_V_format_22 CVCL_V_format_47))) (or (not (= ?v_23 ?v_47)) (= CVCL_V_format_23 CVCL_V_format_47))) (or (not (= ?v_24 ?v_47)) (= CVCL_V_format_24 CVCL_V_format_47))) (or (not (= ?v_25 ?v_47)) (= CVCL_V_format_25 CVCL_V_format_47))) (or (not (= ?v_26 ?v_47)) (= CVCL_V_format_26 CVCL_V_format_47))) (or (not (= ?v_27 ?v_47)) (= CVCL_V_format_27 CVCL_V_format_47))) (or (not (= ?v_28 ?v_47)) (= CVCL_V_format_28 CVCL_V_format_47))) (or (not (= ?v_29 ?v_47)) (= CVCL_V_format_29 CVCL_V_format_47))) (or (not (= ?v_30 ?v_47)) (= CVCL_V_format_30 CVCL_V_format_47))) (or (not (= ?v_31 ?v_47)) (= CVCL_V_format_31 CVCL_V_format_47))) (or (not (= ?v_32 ?v_47)) (= CVCL_V_format_32 CVCL_V_format_47))) (or (not (= ?v_33 ?v_47)) (= CVCL_V_format_33 CVCL_V_format_47))) (or (not (= ?v_34 ?v_47)) (= CVCL_V_format_34 CVCL_V_format_47))) (or (not (= ?v_35 ?v_47)) (= CVCL_V_format_35 CVCL_V_format_47))) (or (not (= ?v_36 ?v_47)) (= CVCL_V_format_36 CVCL_V_format_47))) (or (not (= ?v_37 ?v_47)) (= CVCL_V_format_37 CVCL_V_format_47))) (or (not (= ?v_38 ?v_47)) (= CVCL_V_format_38 CVCL_V_format_47))) (or (not (= ?v_39 ?v_47)) (= CVCL_V_format_39 CVCL_V_format_47))) (or (not (= ?v_40 ?v_47)) (= CVCL_V_format_40 CVCL_V_format_47))) (or (not (= ?v_43 ?v_47)) (= CVCL_V_format_41 CVCL_V_format_47))) (or (not (= CVCL_fmt1 ?v_47)) (= CVCL_V_format_42 CVCL_V_format_47))) (or (not (= ?v_42 ?v_47)) (= CVCL_V_format_43 CVCL_V_format_47)))) (or (not (and (and (and (and (and (and (and (and (and (and (= CVCL_distance (bvadd ((_ extract 31 0) (_ bv50 32)) CVCL_ZERO_)) (= CVCL_fmt_length ?v_43)) (= CVCL_adr_lo ?v_4)) (= CVCL_adr_medlo ?v_5)) (= CVCL_adr_medhi ?v_6)) (= CVCL_adr_hi ?v_7)) (and (= CVCL_percent ?v_38) (= CVCL_s (bvadd ((_ extract 31 0) (_ bv115 32)) CVCL_ZERO_)))) (and (and (and (and (and (and (and (= CVCL_fmt0 CVCL_ZERO_) (= CVCL_arg0 (bvsub CVCL_fmt0 CVCL_distance))) (or (bvult CVCL_arg1 CVCL_fmt0) (= CVCL_arg1 CVCL_fmt0))) (bvult (bvsub (bvadd CVCL_fmt0 CVCL_fmt_length) ?v_2) CVCL_fmt1)) (bvult CVCL_fmt1 (bvadd ?v_41 CVCL_fmt0))) (or (bvult CVCL_arg1 ?v_48) (= CVCL_arg1 ?v_48))) (bvult (bvsub (bvadd ?v_48 CVCL_fmt_length) ?v_5) CVCL_arg1)) (= CVCL_arg1 (bvadd CVCL_arg0 (bvmul ?v_49 CVCL_V_s_count_1))))) (and (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (= CVCL_fmt1 ?v_50) (= CVCL_fmt1 ?v_51)) (= CVCL_fmt1 ?v_52)) (= CVCL_fmt1 ?v_53)) (= CVCL_fmt1 ?v_54)) (= CVCL_fmt1 ?v_55)) (= CVCL_fmt1 ?v_56)) (= CVCL_fmt1 ?v_57)) (= CVCL_fmt1 ?v_58)) (= CVCL_fmt1 ?v_59)) (= CVCL_fmt1 ?v_60)) (= CVCL_fmt1 ?v_61)) (= CVCL_fmt1 ?v_62)) (= CVCL_fmt1 ?v_63)) (= CVCL_fmt1 ?v_64)) (= CVCL_fmt1 ?v_65)) (= CVCL_fmt1 ?v_66)) (= CVCL_fmt1 ?v_67)) (= CVCL_fmt1 ?v_68)) (= CVCL_fmt1 ?v_69)) (= CVCL_fmt1 ?v_70)) (= CVCL_fmt1 ?v_71)) (= CVCL_fmt1 ?v_72)) (= CVCL_fmt1 ?v_73)) (= CVCL_fmt1 ?v_74)) (= CVCL_fmt1 ?v_75)) (= CVCL_fmt1 ?v_76)) (= CVCL_fmt1 ?v_77)) (= CVCL_fmt1 ?v_78)) (= CVCL_fmt1 ?v_79)) (= CVCL_fmt1 ?v_80)) (= CVCL_fmt1 ?v_81)) (= CVCL_fmt1 ?v_82)) (= CVCL_fmt1 ?v_83)) (= CVCL_fmt1 ?v_84)) (= CVCL_fmt1 ?v_85)) (= CVCL_fmt1 ?v_86)) (= CVCL_fmt1 (bvadd CVCL_fmt0 ?v_38))) (= CVCL_fmt1 (bvadd CVCL_fmt0 ?v_39))) (= CVCL_fmt1 (bvadd CVCL_fmt0 ?v_40))) (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (= CVCL_arg1 ?v_50) (= CVCL_arg1 ?v_51)) (= CVCL_arg1 ?v_52)) (= CVCL_arg1 ?v_53)) (= CVCL_arg1 ?v_54)) (= CVCL_arg1 ?v_55)) (= CVCL_arg1 ?v_56)) (= CVCL_arg1 ?v_57)) (= CVCL_arg1 ?v_58)) (= CVCL_arg1 ?v_59)) (= CVCL_arg1 ?v_60)) (= CVCL_arg1 ?v_61)) (= CVCL_arg1 ?v_62)) (= CVCL_arg1 ?v_63)) (= CVCL_arg1 ?v_64)) (= CVCL_arg1 ?v_65)) (= CVCL_arg1 ?v_66)) (= CVCL_arg1 ?v_67)) (= CVCL_arg1 ?v_68)) (= CVCL_arg1 ?v_69)) (= CVCL_arg1 ?v_70)) (= CVCL_arg1 ?v_71)) (= CVCL_arg1 ?v_72)) (= CVCL_arg1 ?v_73)) (= CVCL_arg1 ?v_74)) (= CVCL_arg1 ?v_75)) (= CVCL_arg1 ?v_76)) (= CVCL_arg1 ?v_77)) (= CVCL_arg1 ?v_78)) (= CVCL_arg1 ?v_79)) (= CVCL_arg1 ?v_80)) (= CVCL_arg1 ?v_81)) (= CVCL_arg1 ?v_82)) (= CVCL_arg1 ?v_83)) (= CVCL_arg1 ?v_84)) (= CVCL_arg1 ?v_85)) (= CVCL_arg1 ?v_86)))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (or (or (or (or (or (or ?v_88 (= CVCL_V_format_1 CVCL_s)) (= CVCL_V_format_1 ?v_4)) (= CVCL_V_format_1 ?v_5)) (= CVCL_V_format_1 ?v_6)) (= CVCL_V_format_1 ?v_7)) (= CVCL_V_format_1 ?v_87)) (or (or (or (or (or (or ?v_91 ?v_89) (= CVCL_V_format_2 ?v_4)) (= CVCL_V_format_2 ?v_5)) (= CVCL_V_format_2 ?v_6)) (= CVCL_V_format_2 ?v_7)) (= CVCL_V_format_2 ?v_87))) (or (or (or (or (or (or ?v_94 ?v_92) (= CVCL_V_format_3 ?v_4)) (= CVCL_V_format_3 ?v_5)) (= CVCL_V_format_3 ?v_6)) (= CVCL_V_format_3 ?v_7)) (= CVCL_V_format_3 ?v_87))) (or (or (or (or (or (or ?v_97 ?v_95) (= CVCL_V_format_4 ?v_4)) (= CVCL_V_format_4 ?v_5)) (= CVCL_V_format_4 ?v_6)) (= CVCL_V_format_4 ?v_7)) (= CVCL_V_format_4 ?v_87))) (or (or (or (or (or (or ?v_100 ?v_98) (= CVCL_V_format_5 ?v_4)) (= CVCL_V_format_5 ?v_5)) (= CVCL_V_format_5 ?v_6)) (= CVCL_V_format_5 ?v_7)) (= CVCL_V_format_5 ?v_87))) (or (or (or (or (or (or ?v_103 ?v_101) (= CVCL_V_format_6 ?v_4)) (= CVCL_V_format_6 ?v_5)) (= CVCL_V_format_6 ?v_6)) (= CVCL_V_format_6 ?v_7)) (= CVCL_V_format_6 ?v_87))) (or (or (or (or (or (or ?v_106 ?v_104) (= CVCL_V_format_7 ?v_4)) (= CVCL_V_format_7 ?v_5)) (= CVCL_V_format_7 ?v_6)) (= CVCL_V_format_7 ?v_7)) (= CVCL_V_format_7 ?v_87))) (or (or (or (or (or (or ?v_109 ?v_107) (= CVCL_V_format_8 ?v_4)) (= CVCL_V_format_8 ?v_5)) (= CVCL_V_format_8 ?v_6)) (= CVCL_V_format_8 ?v_7)) (= CVCL_V_format_8 ?v_87))) (or (or (or (or (or (or ?v_112 ?v_110) (= CVCL_V_format_9 ?v_4)) (= CVCL_V_format_9 ?v_5)) (= CVCL_V_format_9 ?v_6)) (= CVCL_V_format_9 ?v_7)) (= CVCL_V_format_9 ?v_87))) (or (or (or (or (or (or ?v_115 ?v_113) (= CVCL_V_format_10 ?v_4)) (= CVCL_V_format_10 ?v_5)) (= CVCL_V_format_10 ?v_6)) (= CVCL_V_format_10 ?v_7)) (= CVCL_V_format_10 ?v_87))) (or (or (or (or (or (or ?v_118 ?v_116) (= CVCL_V_format_11 ?v_4)) (= CVCL_V_format_11 ?v_5)) (= CVCL_V_format_11 ?v_6)) (= CVCL_V_format_11 ?v_7)) (= CVCL_V_format_11 ?v_87))) (or (or (or (or (or (or ?v_121 ?v_119) (= CVCL_V_format_12 ?v_4)) (= CVCL_V_format_12 ?v_5)) (= CVCL_V_format_12 ?v_6)) (= CVCL_V_format_12 ?v_7)) (= CVCL_V_format_12 ?v_87))) (or (or (or (or (or (or ?v_124 ?v_122) (= CVCL_V_format_13 ?v_4)) (= CVCL_V_format_13 ?v_5)) (= CVCL_V_format_13 ?v_6)) (= CVCL_V_format_13 ?v_7)) (= CVCL_V_format_13 ?v_87))) (or (or (or (or (or (or ?v_127 ?v_125) (= CVCL_V_format_14 ?v_4)) (= CVCL_V_format_14 ?v_5)) (= CVCL_V_format_14 ?v_6)) (= CVCL_V_format_14 ?v_7)) (= CVCL_V_format_14 ?v_87))) (or (or (or (or (or (or ?v_130 ?v_128) (= CVCL_V_format_15 ?v_4)) (= CVCL_V_format_15 ?v_5)) (= CVCL_V_format_15 ?v_6)) (= CVCL_V_format_15 ?v_7)) (= CVCL_V_format_15 ?v_87))) (or (or (or (or (or (or ?v_133 ?v_131) (= CVCL_V_format_16 ?v_4)) (= CVCL_V_format_16 ?v_5)) (= CVCL_V_format_16 ?v_6)) (= CVCL_V_format_16 ?v_7)) (= CVCL_V_format_16 ?v_87))) (or (or (or (or (or (or ?v_136 ?v_134) (= CVCL_V_format_17 ?v_4)) (= CVCL_V_format_17 ?v_5)) (= CVCL_V_format_17 ?v_6)) (= CVCL_V_format_17 ?v_7)) (= CVCL_V_format_17 ?v_87))) (or (or (or (or (or (or ?v_139 ?v_137) (= CVCL_V_format_18 ?v_4)) (= CVCL_V_format_18 ?v_5)) (= CVCL_V_format_18 ?v_6)) (= CVCL_V_format_18 ?v_7)) (= CVCL_V_format_18 ?v_87))) (or (or (or (or (or (or ?v_142 ?v_140) (= CVCL_V_format_19 ?v_4)) (= CVCL_V_format_19 ?v_5)) (= CVCL_V_format_19 ?v_6)) (= CVCL_V_format_19 ?v_7)) (= CVCL_V_format_19 ?v_87))) (or (or (or (or (or (or ?v_145 ?v_143) (= CVCL_V_format_20 ?v_4)) (= CVCL_V_format_20 ?v_5)) (= CVCL_V_format_20 ?v_6)) (= CVCL_V_format_20 ?v_7)) (= CVCL_V_format_20 ?v_87))) (or (or (or (or (or (or ?v_148 ?v_146) (= CVCL_V_format_21 ?v_4)) (= CVCL_V_format_21 ?v_5)) (= CVCL_V_format_21 ?v_6)) (= CVCL_V_format_21 ?v_7)) (= CVCL_V_format_21 ?v_87))) (or (or (or (or (or (or ?v_151 ?v_149) (= CVCL_V_format_22 ?v_4)) (= CVCL_V_format_22 ?v_5)) (= CVCL_V_format_22 ?v_6)) (= CVCL_V_format_22 ?v_7)) (= CVCL_V_format_22 ?v_87))) (or (or (or (or (or (or ?v_154 ?v_152) (= CVCL_V_format_23 ?v_4)) (= CVCL_V_format_23 ?v_5)) (= CVCL_V_format_23 ?v_6)) (= CVCL_V_format_23 ?v_7)) (= CVCL_V_format_23 ?v_87))) (or (or (or (or (or (or ?v_157 ?v_155) (= CVCL_V_format_24 ?v_4)) (= CVCL_V_format_24 ?v_5)) (= CVCL_V_format_24 ?v_6)) (= CVCL_V_format_24 ?v_7)) (= CVCL_V_format_24 ?v_87))) (or (or (or (or (or (or ?v_160 ?v_158) (= CVCL_V_format_25 ?v_4)) (= CVCL_V_format_25 ?v_5)) (= CVCL_V_format_25 ?v_6)) (= CVCL_V_format_25 ?v_7)) (= CVCL_V_format_25 ?v_87))) (or (or (or (or (or (or ?v_163 ?v_161) (= CVCL_V_format_26 ?v_4)) (= CVCL_V_format_26 ?v_5)) (= CVCL_V_format_26 ?v_6)) (= CVCL_V_format_26 ?v_7)) (= CVCL_V_format_26 ?v_87))) (or (or (or (or (or (or ?v_166 ?v_164) (= CVCL_V_format_27 ?v_4)) (= CVCL_V_format_27 ?v_5)) (= CVCL_V_format_27 ?v_6)) (= CVCL_V_format_27 ?v_7)) (= CVCL_V_format_27 ?v_87))) (or (or (or (or (or (or ?v_169 ?v_167) (= CVCL_V_format_28 ?v_4)) (= CVCL_V_format_28 ?v_5)) (= CVCL_V_format_28 ?v_6)) (= CVCL_V_format_28 ?v_7)) (= CVCL_V_format_28 ?v_87))) (or (or (or (or (or (or ?v_172 ?v_170) (= CVCL_V_format_29 ?v_4)) (= CVCL_V_format_29 ?v_5)) (= CVCL_V_format_29 ?v_6)) (= CVCL_V_format_29 ?v_7)) (= CVCL_V_format_29 ?v_87))) (or (or (or (or (or (or ?v_175 ?v_173) (= CVCL_V_format_30 ?v_4)) (= CVCL_V_format_30 ?v_5)) (= CVCL_V_format_30 ?v_6)) (= CVCL_V_format_30 ?v_7)) (= CVCL_V_format_30 ?v_87))) (or (or (or (or (or (or ?v_178 ?v_176) (= CVCL_V_format_31 ?v_4)) (= CVCL_V_format_31 ?v_5)) (= CVCL_V_format_31 ?v_6)) (= CVCL_V_format_31 ?v_7)) (= CVCL_V_format_31 ?v_87))) (or (or (or (or (or (or ?v_181 ?v_179) (= CVCL_V_format_32 ?v_4)) (= CVCL_V_format_32 ?v_5)) (= CVCL_V_format_32 ?v_6)) (= CVCL_V_format_32 ?v_7)) (= CVCL_V_format_32 ?v_87))) (or (or (or (or (or (or ?v_184 ?v_182) (= CVCL_V_format_33 ?v_4)) (= CVCL_V_format_33 ?v_5)) (= CVCL_V_format_33 ?v_6)) (= CVCL_V_format_33 ?v_7)) (= CVCL_V_format_33 ?v_87))) (or (or (or (or (or (or ?v_187 ?v_185) (= CVCL_V_format_34 ?v_4)) (= CVCL_V_format_34 ?v_5)) (= CVCL_V_format_34 ?v_6)) (= CVCL_V_format_34 ?v_7)) (= CVCL_V_format_34 ?v_87))) (or (or (or (or (or (or ?v_190 ?v_188) (= CVCL_V_format_35 ?v_4)) (= CVCL_V_format_35 ?v_5)) (= CVCL_V_format_35 ?v_6)) (= CVCL_V_format_35 ?v_7)) (= CVCL_V_format_35 ?v_87))) (or (or (or (or (or (or ?v_193 ?v_191) (= CVCL_V_format_36 ?v_4)) (= CVCL_V_format_36 ?v_5)) (= CVCL_V_format_36 ?v_6)) (= CVCL_V_format_36 ?v_7)) (= CVCL_V_format_36 ?v_87))) (or (or (or (or (or (or ?v_196 ?v_194) (= CVCL_V_format_37 ?v_4)) (= CVCL_V_format_37 ?v_5)) (= CVCL_V_format_37 ?v_6)) (= CVCL_V_format_37 ?v_7)) (= CVCL_V_format_37 ?v_87))) (or (or (or (or (or (or ?v_199 ?v_197) (= CVCL_V_format_38 ?v_4)) (= CVCL_V_format_38 ?v_5)) (= CVCL_V_format_38 ?v_6)) (= CVCL_V_format_38 ?v_7)) (= CVCL_V_format_38 ?v_87))) (or (or (or (or (or (or ?v_202 ?v_200) (= CVCL_V_format_39 ?v_4)) (= CVCL_V_format_39 ?v_5)) (= CVCL_V_format_39 ?v_6)) (= CVCL_V_format_39 ?v_7)) (= CVCL_V_format_39 ?v_87))) (or (or (or (or (or (or ?v_205 ?v_203) (= CVCL_V_format_40 ?v_4)) (= CVCL_V_format_40 ?v_5)) (= CVCL_V_format_40 ?v_6)) (= CVCL_V_format_40 ?v_7)) (= CVCL_V_format_40 ?v_87)))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (or (not ?v_90) (= CVCL_V_s_count_2 ?v_2)) (or ?v_90 (= CVCL_V_s_count_2 CVCL_ZERO_))) (and (or (not ?v_93) (= CVCL_V_s_count_3 (bvadd CVCL_V_s_count_2 ?v_2))) (or ?v_93 (= CVCL_V_s_count_2 CVCL_V_s_count_3)))) (and (or (not ?v_96) (= CVCL_V_s_count_4 (bvadd CVCL_V_s_count_3 ?v_2))) (or ?v_96 (= CVCL_V_s_count_3 CVCL_V_s_count_4)))) (and (or (not ?v_99) (= CVCL_V_s_count_5 (bvadd CVCL_V_s_count_4 ?v_2))) (or ?v_99 (= CVCL_V_s_count_4 CVCL_V_s_count_5)))) (and (or (not ?v_102) (= CVCL_V_s_count_6 (bvadd CVCL_V_s_count_5 ?v_2))) (or ?v_102 (= CVCL_V_s_count_5 CVCL_V_s_count_6)))) (and (or (not ?v_105) (= CVCL_V_s_count_7 (bvadd CVCL_V_s_count_6 ?v_2))) (or ?v_105 (= CVCL_V_s_count_6 CVCL_V_s_count_7)))) (and (or (not ?v_108) (= CVCL_V_s_count_8 (bvadd CVCL_V_s_count_7 ?v_2))) (or ?v_108 (= CVCL_V_s_count_7 CVCL_V_s_count_8)))) (and (or (not ?v_111) (= CVCL_V_s_count_9 (bvadd CVCL_V_s_count_8 ?v_2))) (or ?v_111 (= CVCL_V_s_count_8 CVCL_V_s_count_9)))) (and (or (not ?v_114) (= CVCL_V_s_count_10 (bvadd CVCL_V_s_count_9 ?v_2))) (or ?v_114 (= CVCL_V_s_count_9 CVCL_V_s_count_10)))) (and (or (not ?v_117) (= CVCL_V_s_count_11 (bvadd CVCL_V_s_count_10 ?v_2))) (or ?v_117 (= CVCL_V_s_count_10 CVCL_V_s_count_11)))) (and (or (not ?v_120) (= CVCL_V_s_count_12 (bvadd CVCL_V_s_count_11 ?v_2))) (or ?v_120 (= CVCL_V_s_count_11 CVCL_V_s_count_12)))) (and (or (not ?v_123) (= CVCL_V_s_count_13 (bvadd CVCL_V_s_count_12 ?v_2))) (or ?v_123 (= CVCL_V_s_count_12 CVCL_V_s_count_13)))) (and (or (not ?v_126) (= CVCL_V_s_count_14 (bvadd CVCL_V_s_count_13 ?v_2))) (or ?v_126 (= CVCL_V_s_count_13 CVCL_V_s_count_14)))) (and (or (not ?v_129) (= CVCL_V_s_count_15 (bvadd CVCL_V_s_count_14 ?v_2))) (or ?v_129 (= CVCL_V_s_count_14 CVCL_V_s_count_15)))) (and (or (not ?v_132) (= CVCL_V_s_count_16 (bvadd CVCL_V_s_count_15 ?v_2))) (or ?v_132 (= CVCL_V_s_count_15 CVCL_V_s_count_16)))) (and (or (not ?v_135) (= CVCL_V_s_count_17 (bvadd CVCL_V_s_count_16 ?v_2))) (or ?v_135 (= CVCL_V_s_count_16 CVCL_V_s_count_17)))) (and (or (not ?v_138) (= CVCL_V_s_count_18 (bvadd CVCL_V_s_count_17 ?v_2))) (or ?v_138 (= CVCL_V_s_count_17 CVCL_V_s_count_18)))) (and (or (not ?v_141) (= CVCL_V_s_count_19 (bvadd CVCL_V_s_count_18 ?v_2))) (or ?v_141 (= CVCL_V_s_count_18 CVCL_V_s_count_19)))) (and (or (not ?v_144) (= CVCL_V_s_count_20 (bvadd CVCL_V_s_count_19 ?v_2))) (or ?v_144 (= CVCL_V_s_count_19 CVCL_V_s_count_20)))) (and (or (not ?v_147) (= CVCL_V_s_count_21 (bvadd CVCL_V_s_count_20 ?v_2))) (or ?v_147 (= CVCL_V_s_count_20 CVCL_V_s_count_21)))) (and (or (not ?v_150) (= CVCL_V_s_count_22 (bvadd CVCL_V_s_count_21 ?v_2))) (or ?v_150 (= CVCL_V_s_count_21 CVCL_V_s_count_22)))) (and (or (not ?v_153) (= CVCL_V_s_count_23 (bvadd CVCL_V_s_count_22 ?v_2))) (or ?v_153 (= CVCL_V_s_count_22 CVCL_V_s_count_23)))) (and (or (not ?v_156) (= CVCL_V_s_count_24 (bvadd CVCL_V_s_count_23 ?v_2))) (or ?v_156 (= CVCL_V_s_count_23 CVCL_V_s_count_24)))) (and (or (not ?v_159) (= CVCL_V_s_count_25 (bvadd CVCL_V_s_count_24 ?v_2))) (or ?v_159 (= CVCL_V_s_count_24 CVCL_V_s_count_25)))) (and (or (not ?v_162) (= CVCL_V_s_count_26 (bvadd CVCL_V_s_count_25 ?v_2))) (or ?v_162 (= CVCL_V_s_count_25 CVCL_V_s_count_26)))) (and (or (not ?v_165) (= CVCL_V_s_count_27 (bvadd CVCL_V_s_count_26 ?v_2))) (or ?v_165 (= CVCL_V_s_count_26 CVCL_V_s_count_27)))) (and (or (not ?v_168) (= CVCL_V_s_count_28 (bvadd CVCL_V_s_count_27 ?v_2))) (or ?v_168 (= CVCL_V_s_count_27 CVCL_V_s_count_28)))) (and (or (not ?v_171) (= CVCL_V_s_count_29 (bvadd CVCL_V_s_count_28 ?v_2))) (or ?v_171 (= CVCL_V_s_count_28 CVCL_V_s_count_29)))) (and (or (not ?v_174) (= CVCL_V_s_count_30 (bvadd CVCL_V_s_count_29 ?v_2))) (or ?v_174 (= CVCL_V_s_count_29 CVCL_V_s_count_30)))) (and (or (not ?v_177) (= CVCL_V_s_count_31 (bvadd CVCL_V_s_count_30 ?v_2))) (or ?v_177 (= CVCL_V_s_count_30 CVCL_V_s_count_31)))) (and (or (not ?v_180) (= CVCL_V_s_count_32 (bvadd CVCL_V_s_count_31 ?v_2))) (or ?v_180 (= CVCL_V_s_count_31 CVCL_V_s_count_32)))) (and (or (not ?v_183) (= CVCL_V_s_count_33 (bvadd CVCL_V_s_count_32 ?v_2))) (or ?v_183 (= CVCL_V_s_count_32 CVCL_V_s_count_33)))) (and (or (not ?v_186) (= CVCL_V_s_count_34 (bvadd CVCL_V_s_count_33 ?v_2))) (or ?v_186 (= CVCL_V_s_count_33 CVCL_V_s_count_34)))) (and (or (not ?v_189) (= CVCL_V_s_count_35 (bvadd CVCL_V_s_count_34 ?v_2))) (or ?v_189 (= CVCL_V_s_count_34 CVCL_V_s_count_35)))) (and (or (not ?v_192) (= CVCL_V_s_count_36 (bvadd CVCL_V_s_count_35 ?v_2))) (or ?v_192 (= CVCL_V_s_count_35 CVCL_V_s_count_36)))) (and (or (not ?v_195) (= CVCL_V_s_count_37 (bvadd CVCL_V_s_count_36 ?v_2))) (or ?v_195 (= CVCL_V_s_count_36 CVCL_V_s_count_37)))) (and (or (not ?v_198) (= CVCL_V_s_count_38 (bvadd CVCL_V_s_count_37 ?v_2))) (or ?v_198 (= CVCL_V_s_count_37 CVCL_V_s_count_38)))) (and (or (not ?v_201) (= CVCL_V_s_count_39 (bvadd CVCL_V_s_count_38 ?v_2))) (or ?v_201 (= CVCL_V_s_count_38 CVCL_V_s_count_39)))) (and (or (not ?v_204) (= CVCL_V_s_count_40 (bvadd CVCL_V_s_count_39 ?v_2))) (or ?v_204 (= CVCL_V_s_count_39 CVCL_V_s_count_40)))) (and (or (not ?v_206) (= CVCL_V_s_count_41 (bvadd CVCL_V_s_count_40 ?v_2))) (or ?v_206 (= CVCL_V_s_count_40 CVCL_V_s_count_41)))))) (and (and (and (and (and (not (= CVCL_V_format_42 CVCL_percent)) (= CVCL_V_format_43 CVCL_s)) (= CVCL_V_format_44 CVCL_adr_lo)) (= CVCL_V_format_45 CVCL_adr_medlo)) (= CVCL_V_format_46 CVCL_adr_medhi)) (= CVCL_V_format_47 CVCL_adr_hi)))))))))))))
(check-sat)
(set-option :regular-output-channel "/dev/null")
(get-model)
(exit)
